#|===== Usage Note ===================================================
 Where to put this file:
 
   * SE-Projects (this name does not matter)
   |- SE    (must use this name)
   |  |- binary-io-utilities.lisp
   |
   |- iEx0  (name does not matter)
   |  |- iEx0.ezpsp
   |  |- iEx0.lisp
   |
   |- iEx1  (name does not matter)
   |  |- iEx1.ezpsp
   |  |- iEx1.lisp
   | 
   | etc...

 To certify: open this module in DrACuLa and press Save/Certify

 To make definitions in this module available in a module residing
 in iEx0, iEx1, ..., put the following commands in that module:
   (include-book "../SE/binary-io-utilities")
   (set-state-ok t)

 Limitations
   binary-file->byte-list is designed to read files up to 4GB,
   but may trigger problems on some systems, even on smaller files.
   Testing, so far, has succeeded on 2MB files, but failed on 25MB 
   files.
======================================================================

===== Environment setup ============================================|#

  (in-package "ACL2")
  (set-compile-fns t)
  (set-state-ok t)
#|==================================================================|#


(defun read-n-bytes (n bytes-already-in channel state)
   (if (or (not (integerp n)) (<= n 0))
       (mv bytes-already-in channel state)
       (mv-let (byte state) (read-byte$ channel state)
          (if (null byte)
              (mv bytes-already-in channel state)
              (read-n-bytes (- n 1)
                            (cons byte bytes-already-in) 
                            channel state)))))

(defconst *max-file-size* 4000000000) ;limits input file to 4GB
(defun binary-file->byte-list (fname state)
   (mv-let (byte-list error state)
           (mv-let (channel state) 
                   (open-input-channel fname :byte state)
              (if (null channel)
                  (mv nil
                      (string-append 
                               "Error while opening file for input: "
                               fname)
                      state)
                  (mv-let (byte-list chnl state)
                          (read-n-bytes *max-file-size* 
                                        '() channel state)
                     (let ((state (close-input-channel chnl state)))
                       (mv byte-list nil state)))))
      (mv (reverse byte-list) error state)))

(defun binary-write (byte-list channel state)
  (if (atom byte-list)
      (mv channel state)
      (let ((state (write-byte$ (car byte-list) channel state)))
         (binary-write (cdr byte-list) channel state))))

(defun byte-list->binary-file (fname byte-list state)
  (mv-let (channel state)
          (open-output-channel fname :byte state)
     (if (null channel)
         (mv (string-append "Error while opening file for output: " 
                            fname)
             state)
         (mv-let (channel state)
                 (binary-write byte-list channel state)
            (let ((state (close-output-channel channel state)))
              (mv nil state))))))

#|===== Unit test framework ==========================================
======================================================================
 Implementation note
   ACL2 has special display rules for multiple-values of
   multiplicity three when the last component is state.
   To avoid these rules, state is the first component
   in the multiple-value delivered by r-bmp 
====================================================================|#
(defun r-bmp (state)
  (mv-let (input-bytes error-open state)
          (binary-file->byte-list "C:/temp/imgIn.bmp" state)
     (if error-open
         (mv state error-open nil)
         (mv state
             (string-append "Success: read c:/imgIn.bmp"
                            (coerce '(#\newline) 'STRING))
              input-bytes))))

(defun rw-bmp (state)
  (mv-let (input-bytes error-open state)
          (binary-file->byte-list "C:/temp/imgIn.bmp" state)
     (if error-open
         (mv error-open state)
         (mv-let (error-close state)
                 (byte-list->binary-file "C:/temp/imgOut.bmp"
                                         input-bytes
                                         state)
            (if error-close
                (mv error-close state)
                (mv nil state))))))

(defun zap-bit (byte)
  (logand #b11111110 (char-code (code-char byte))))

#| Warning! To avoid stack overflow, issue the command
            :comp zap-bits
          after importing these functions
 Implementation note
   The function zap-bits is tail recursive, and this
   is a crucial factor in applying it to long lists of bytes
   It would fail on lists longer than about 30,000 bytes
   if it were not tail recursive. |#
(defun zap-bits (skip bytes zapped)
  (if (endp bytes)
      (reverse zapped)
      (if (zp skip)
          (zap-bits 0 (cdr bytes) 
                   (cons (zap-bit (car bytes)) zapped))
          (zap-bits (- skip 1) (cdr bytes) 
                    (cons (car bytes) zapped)))))

#| (zap-img bmp-in bmp-out state)
 writes a copy of the BMP image file at
 the path specified in the string bmp-in
 to the path specified in the string bmp-out,
 but with all low order bits in bytes beyond 
 the 1000th byte set to zero
 Warning! To avoid stack overflow, issue the command
            :comp zap-bits
          after importing these functions |#
(defun zap-img (img-in img-out state)
  (mv-let (input-bytes error-open state)
          (binary-file->byte-list img-in state)
     (if error-open
         (mv error-open state)
         (mv-let (error-close state)
                 (byte-list->binary-file img-out
                                         (zap-bits 1000 
                                                   input-bytes nil)
                                         state)
            (if error-close
                (mv error-close state)
                (mv nil state))))))
#|==================================================================|#
